| Definitions | t  T, x:A  B(x),  x:A. B(x), Msg, w.M, Msg(M), Id, s = t, {x:A| B(x)} , P   Q, False,  A, A  B,  ,  , Type, IdLnk, vartype(i;x), M(i), M.ds(x), S  T,  , suptype(S; T), s(i;t).x,  x.A(x), timedState(ds), M.(timed)state, f(a), Top, if b then t else f fi , valtype(i;a), M.da(a), val(a), Valtype(da;k), M.V(k), #$n, n+m, a < b, Void, r - s, type List, [], mlnk(m), source(l), m(i;t), onlnk(l;mss), M.bframe(k sends on l),  b, w-machine-independent(w;i;k;x), M.rframe(k reads x), Knd, x:A  B(x), P & Q, r + s, M.aframe(k affects x), isnull(a), read-state(s), unsolvable M.pre(a,s), a declared in M, left + right, P  Q, A c B,  x:A. B(x), w-tagged(tg;mss), M.sframe(k sends <l,tg>), M.frame(k affects x), rcv(l,tg), a = b, withlnk(l;mss), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), w-knum(w;i;k;t), ma-random(M;T;v;i;a;n), M.pre(a,s), islocal(k), M.init(x,v), Action(i),  , FairFifo, PossibleWorld(D;w), Dsys, World, a(i;t), kind(a), act(k), locl(a), s ~ t, z != f(x) P(a;z), Atom$n, w-action-dec(TA;M;i), Action(dec), w-automaton(T;TA;M),  , let x,y = A in B(x;y),  x:A.B(x),  b, P  Q, Unit |
| Lemmas | eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bool wf, bnot wf, world wf, dsys wf, fair-fifo wf, ma-ds wf, w-action wf, ma-init wf, islocal wf, ma-pre wf, ma-random wf, w-valtype wf, actof wf, w-knum wf, ma-ef wf, ma-send wf, w-withlnk wf, ifthenelse wf, eq id wf, ma-da wf, rcv wf, top wf, ma-frame wf, ma-sframe wf, w-tagged wf, locl wf, ma-decla wf2, ma-npre wf, read-state wf, nat wf, assert wf, w-isnull wf, w-a wf, ma-aframe wf, qadd wf, Knd wf, ma-rframe wf, w-machine-independent wf, not wf, ma-bframe wf, d-m wf, w-kind wf, w-Msg wf, w-onlnk wf, w-m wf, Msg wf, w-M wf, lsrc wf, mlnk wf, qsub wf, int inc rationals, le wf, w-val wf, w-s wf, rationals wf, w-vartype wf, IdLnk wf, Id wf |